a, b:Knd. a = b  a = b 

latex

Definitions	Knd, P  Q, P  Q, P & Q, P  Q, Prop, t  T, KindDeq, x:A. B(x), eqof(d), b, a = b
Lemmas	Knd wf, iff functionality wrt iff, deq property, assert wf, eqof wf, Kind-deq wf